\begin{tabbing}
R{-}Feasible\=\{i:l\}\+
\\[0ex]($R$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$es\_realizer\_ind(\=$R$;\+
\\[0ex]True;
\\[0ex]${\it left}$,${\it right}$,${\it rec}_{1}$,${\it rec}_{2}$.(${\it rec}_{1}$ $\wedge$ ${\it rec}_{2}$ $\wedge$ R{-}compat\{i:l\}(${\it left}$; ${\it right}$));
\\[0ex]${\it loc}$,$T$,$x$,$v$.True;
\\[0ex]${\it loc}$,$T$,$x$,$L$.normal{-}type\=\{i:l\}\+
\\[0ex]($T$);
\-\\[0ex]${\it lnk}$,${\it tag}$,$L$.True;
\\[0ex]${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$.((normal{-}ds\{i:l\}(${\it ds}$) $\wedge$ normal{-}type\{i:l\}($T$))
\\[0ex]$\wedge$ (($\uparrow$isrcv(${\it knd}$)) $\Rightarrow$ (${\it loc}$ = destination(lnk(${\it knd}$)) $\in$ Id)));
\\[0ex]${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$.(\=(($\uparrow$isrcv(${\it knd}$))\+
\\[0ex]$\Rightarrow$ \=((($\uparrow$eq\_lnk(lnk(${\it knd}$); $l$))\+
\\[0ex]$\Rightarrow$ (\=$T$\+
\\[0ex]=
\\[0ex]fpf{-}cap(${\it dt}$; id{-}deq; tag(${\it knd}$); void)
\\[0ex]$\in$ Type\{i\}))
\-\\[0ex]$\wedge$ (destination(lnk(${\it knd}$)) = source($l$) $\in$ Id)))
\-\-\\[0ex]$\wedge$ (normal{-}type\{i:l\}($T$) $\wedge$ normal{-}ds\{i:l\}(${\it ds}$))
\\[0ex]$\wedge$ normal{-}ds\=\{i:l\}\+
\\[0ex](${\it dt}$));
\-\\[0ex]${\it loc}$,${\it ds}$,$a$,$T$,$P$.normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$);
\-\\[0ex]${\it loc}$,$k$,$L$.True;
\\[0ex]${\it loc}$,$k$,$L$.True;
\\[0ex]${\it loc}$,$x$,$L$.True)
\-
\end{tabbing}